Inference at * 2 1 1 
Iof proof for Lemma fast-fib:



1. f : 
1. n, a, b:.
1. {m:| 
1. {k:. (a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
  (n.f(n,1,0))  (n:. {m:| m = fib(n)} ) 

latex

 by (RepeatFor (first_nat 1:n) ((MemCD) 
CollapseTHENA (Auto))) 

latex

C1: .....subterm..... T:t1:n

C1: 2. n : 
C1:   f(n,1,0)  {m:| m = fib(n)} 
C.

Definitions	x.A(x), x:A. B(x), t  T,
Lemmas	nat wf